…bled manually

…eanprover#6680)

This PR makes the new code generator skip generating code for decls with
an implemented_by decl, just like the old code generator.

This PR modifies LCNF.toMonoType to use a more refined type erasure
scheme, which distinguishes between irrelevant/erased information
(represented by lcErased) and erased type dependencies (represented by
lcAny). This corresponds to the irrelevant/object distinction in the old
code generator.

This PR deprecates `List.iota`, which we make no essential use of. `iota
n` can be replaced with `(range' 1 n).reverse`. The verification lemmas
for `range'` already have better coverage than those for `iota`.
Any downstream projects using it (I am not aware of any) are encouraged
to adopt it.

This PR changes the identifier parser to allow for the ⱼ unicode
character which was forgotten as it lives by itself in a codeblock with
coptic characters.

…div]` (leanprover#6674)

This PR adds theorems `BitVec.[getMsbD_mul, getElem_udiv, getLsbD_udiv,
getMsbD_udiv]`

---------

Co-authored-by: Siddharth <[email protected]>

…prover#6723)

This PR completes the alignment of
{List/Array/Vector}.{attach,attachWith,pmap} lemmas. I had to fill in a
number of gaps in the List API.

…rse, reverse_append, reverse_replicate` and `Nat.mod_sub_eq_sub_mod` (leanprover#6476)

This PR defines `reverse` for bitvectors and implements a first subset
of theorems (`getLsbD_reverse, getMsbD_reverse, reverse_append,
reverse_replicate, reverse_cast, msb_reverse`). We also include some
necessary related theorems (`cons_append, cons_append_append,
append_assoc, replicate_append_self, replicate_succ'`) and deprecate
theorems`replicate_zero_eq` and `replicate_succ_eq`.

---------

Co-authored-by: Alex Keizer <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

…6355)

This PR adds the ability to define possibly non-terminating functions
and still be able to reason about them equationally, as long as they are
tail-recursive or monadic.

Typical uses of this feature are
```lean4
def ack : (n m : Nat) → Option Nat
  | 0,   y   => some (y+1)
  | x+1, 0   => ack x 1
  | x+1, y+1 => do ack x (← ack (x+1) y)
partial_fixpiont

def whileSome (f : α → Option α) (x : α) : α :=
  match f x with
  | none => x
  | some x' => whileSome f x'
partial_fixpiont

def computeLfp {α : Type u} [DecidableEq α] (f : α → α) (x : α) : α :=
  let next := f x
  if x ≠ next then
    computeLfp f next
  else
    x
partial_fixpiont

noncomputable def geom : Distr Nat := do
  let head ← coin
  if head then
    return 0
  else
    let n ← geom
    return (n + 1)
partial_fixpiont
```

This PR contains

* The necessary fragment of domain theory, up to (a variant of)
Knaster–Tarski theorem (merged as
leanprover#6477)
* A tactic to solve monotonicity goals compositionally (a bit like
mathlib’s `fun_prop`) (merged as
leanprover#6506)
* An attribute to extend that tactic (merged as
leanprover#6506)
* A “derecursifier” that uses that machinery to define recursive
function, including support for dependent functions and mutual
recursion.
* Fixed-point induction principles (technical, tedious to use)
* For `Option`-valued functions: Partial correctness induction theorems
that hide all the domain theory

This is heavily inspired by [Isabelle’s `partial_function`
command](https://isabelle.in.tum.de/doc/codegen.pdf).

…r#6261)

This PR adds `foo.fun_cases`, an automatically generated theorem that
splits the goal according to the branching structure of `foo`, much like
the Functional Induction Principle, but for all functions (not just
recursive ones), and without providing inductive hypotheses.

The design isn't quite final yet as to which function parameters should
become targets of the motive, and which parameters of the theorem, but
the current version is already proven to be useful, so start with this
and iterate later.

This PR adds lemmas about HashMap.alter and .modify. These lemmas
describe the interaction of alter and modify with the read methods of
the HashMap. The additions affect the HashMap, the DHashMap and their
respective raw versions. Moreover, the raw versions of alter and modify
are defined.

---------

Co-authored-by: Paul Reichert <[email protected]>

As @nomeata told me, it should be "try to (...)" because even with
`pp.analyze` roundtripping often fails.

This PR removes theorems `Nat.mul_one` to simplify a rewrite in the
proof of `BitVec.getMsbD_rotateLeft_of_lt`

This PR adds better support for overlapping `match` patterns in `grind`.
`grind` can now solve examples such as
```lean
inductive S where
  | mk1 (n : Nat)
  | mk2 (n : Nat) (s : S)
  | mk3 (n : Bool)
  | mk4 (s1 s2 : S)

def f (x y : S) :=
  match x, y with
  | .mk1 _, _ => 2
  | _, .mk2 1 (.mk4 _ _) => 3
  | .mk3 _, _ => 4
  | _, _ => 5

example : b = .mk2 y1 y2 → y1 = 2 → a = .mk4 y3 y4 → f a b = 5 := by
  unfold f
  grind (splits := 0)
```

---------

Co-authored-by: Leonardo de Moura <[email protected]>

…r#6734)

This PR ensures there are no redundant entries in the offset constraint
model produced by `grind`

… `grind` (leanprover#6735)

This PR adds support for case splitting on `match`-expressions with
overlapping patterns to the `grind` tactic. `grind` can now solve
examples such as:
```
inductive S where
  | mk1 (n : Nat)
  | mk2 (n : Nat) (s : S)
  | mk3 (n : Bool)
  | mk4 (s1 s2 : S)

def g (x y : S) :=
  match x, y with
  | .mk1 a, _ => a + 2
  | _, .mk2 1 (.mk4 _ _) => 3
  | .mk3 _, .mk4 _ _ => 4
  | _, _ => 5

example : g a b > 1 := by
  grind [g.eq_def]
```

This PR ensures the canonicalizer used in `grind` does not waste time
checking whether terms with different types are definitionally equal.

This PR ensures that the branches of an `if-then-else` term are
internalized only after establishing the truth value of the condition.
This change makes its behavior consistent with the `match`-expression
and dependent `if-then-else` behavior in `grind`.
This feature is particularly important for recursive functions defined
by well-founded recursion and `if-then-else`. Without lazy
`if-then-else` branch internalization, the equation theorem for the
recursive function would unfold until reaching the generation depth
threshold, and before performing any case analysis. See new tests for an
example.

…#6724)

This PR adds support for `bv_decide` to automatically split up
non-recursive structures that contain information about supported types.
It can be controlled using the new `structures` field in the `bv_decide`
config.

This PR updates our lexical structure documentation to mention the newly
supported ⱼ which lives in a separate unicode block and is thus not
captured by the current ranges.

…rover#6739)

This PR adds a fast path for bitblasting multiplication with constants
in `bv_decide`.

While the circuit generated is the same (as the AIG already performs
constant folding) this avoids calling out to the shift and addition
bitblaster unless required. Thus the overall time to generate the
circuit is reduced. Inspired by
[bitwuzla](https://github.com/bitwuzla/bitwuzla/blob/25d77f819c84575e6b759db0bbc4ffb2fbb4f20c/src/lib/bitblast/bitblaster.h#L454).

Avoids build time overhead until the option is proven to speed up
average projects. Adds Init.Prelude (many tiny declarations, "worst
case") and Init.List.Sublist (many nontrivial theorems, "best case")
under -DElab.async=true as new benchmarks for tracking.

This PR ensures that conditional equation theorems for function
definitions are handled correctly in `grind`. We use the same
infrastructure built for `match`-expression equations. Recall that in
both cases, these theorems are conditional when there are overlapping
patterns.

This PR adds the lemmas that show what happens when multiplying by
`twoPow` to an arbitrary term, as well to another `twoPow`.

This will be followed up by a PR that uses these to build a simproc to
canonicalize `twoPow w i * x` and `x * twoPow w i`.

This PR supports rewriting `ushiftRight` in terms of `extractLsb'`. This
is the companion PR to leanprover#6743 which adds the similar lemmas about
`shiftLeft`.


```lean
theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) :
    x >>> n = 0#w

theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
    x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega)
```